Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A pseudo-equivalence relation is like an equivalence relation, but where we allow more than one element in the relation; i.e. the underlying directed graph of the relation is a directed pseudograph. In the same way that magmoids are the raw structure used to build semicategories and categories, sets with pseudo-equivalence relations are the raw structure used to build dagger categories and groupoids (i.e. a groupoid without associativity, unital laws, and inverse laws).
Sets equipped with pseudo-equivalence relations are sometimes called setoids (i.e. in Wilander (2012), §4; Palmgren & Wilander (2014), §2, §6; Emmenegger & Palmgren (2020), §6; Cipriano (2020), Def. 1.1.1), but the term “setoid” is also used in mathematics to refer only to the sets with equivalence relations. In this article, the term “setoid” is used in the former sense of “sets equipped with pseudo-equivalence relations”.
Using graph theoretic terminology, a pseudo-equivalence relation on a set of vertices is a family of sets of edges for each vertex and , which comes with the following additional structure
for each vertex an element
for each vertex and a family of functions
for each vertex , , and , a family of functions
A pseuodo-equivalence relation on a set is a set and functions , (a loop directed pseudograph), with with functions , , and
such that
We define an extensional function between two sets and with pseudo-equivalence relations and to be a function and a family of functions
Composition of extensional functions is defined as composition of the vertex function and of each edge function.
An extensional function between two sets with pseudo-equivalence relations is full if every edge function is a surjection, and an extensional function is faithful if every edge function is an injection. An extensional function is injective-on-objects? if the vertex function is an injection, surjective-on-objects if the vertex function is a surjection, and bijective-on-objects if the vertex function is a bijection.
An extensional function is a dagger functor if additionally it preserves the functions , ,
An isomorphism of setoids is a full and faithful bijective-on-objects dagger functor.
Given a one-set-of-edges setoid , we define a family-of-sets-of-edges setoid by taking to be the preimage of under the function . Conversely, given a family-of-sets-of-edges setoid we define a one-set-of-edges setoid by taking to be the disjoint union of the families of edges .
…
The morphisms of a category with a contravariant endofunctor that is the identity-on-objects is a pseudo-equivalence relation where
for every vertex , , , and and edge , , and
for every vertex , and edge
for every vertex , and edge
This includes dagger categories, where additionally
for every vertex , and edge
for every vertex , , and edge ,
for every vertex
and groupoids, where
for every vertex , and edge
for every vertex , and edge
Additionally, a pseudo-equivalence relation on a set with one vertex is equivalent to a pointed magma with an endofunction.
Recall in graph theory that a loop directed pseudograph is simple or a loop digraph if for every vertex and , the set of edges is a subsingleton: for every edge and , . In the other definition, a loop directed pseudograph is a loop digraph if the functions and are jointly monic.
A setoid is thin or simple if its underlying loop directed pseudograph is a loop digraph. In both cases, the pseudo-equivalence relation becomes an equivalence relation. The term “thin” originates from category theory, while the term “simple” originates from graph theory.
A thin setoid is equivalently a thin dagger category, or a dagger category enriched in truth values. A thin setoid is also a thin groupoid, or a groupoid enriched in truth values.
Sometimes in the mathematical literature, setoids are thin by default.
For any pseudo-equivalence relation , the core of is defined as the maximal subgroupoid? of .
More specifically, a sub-pseudo-equivalence relation of a pseudo-equivalence relation is a set with a pseudo-equivalence relation and an faithful injective-on-objects dagger functor . A sub-pseudo-equivalence relation of is a subgroupoid if additionally satisfy the groupoid equational axioms:
for every vertex , , , and and edge , , and
for every vertex , and edge
for every vertex , and edge
for every vertex , and edge
for every vertex , and edge
Every pseudo-equivalence relation has at least one subgroupoid given by only the identity morphisms of . A subgroupoid of a pseudo-equivalence relation is a maximal subgroupoid if the dagger functor is bijective-on-objects, and additionally if, for every other subgroupoid of with faithful injective-on-objects dagger functor , there is a unique faithful injective-on-objects dagger functor such that .
Let the category be defined as a category that is finitely complete and well-pointed (i.e. whose terminal object is a extremal generating object). This category of sets is not even a regular category, let alone an exact category, as can happen in certain foundations of mathematics, such as bare set-level Martin-Löf type theory, or ZFC and ETCS without the powerset axiom. The category of sets with pseudo-equivalence relations is then the ex/lex completion of Set.
More specifically, using the definition of pseudo-equivalence relation with two sets: if and are two pseudo-equivalence relations, a morphism between them in is defined to be a function with functions with and . Moreover, we declare two such functions to be equal if there exists a function such that and . Because is a pseudo-equivalence relation, this defines an actual equivalence relation on the morphisms , which is compatible with composition; thus we have a well-defined category of pseudo-equivalence relations, which is the ex/lex completion of .
We have a full and faithful functor sending an object to the pseudo-equivalence relation . One can then verify directly that is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from into exact categories.
If the presentation axiom (a weak form of the full axiom of choice) holds in , as a subcategory of , could be thought of as the category of completely presented sets, the category of sets with a projective presentation. If the axiom of choice holds in , then is equivalent to , as the axiom of choice implies that is its own free exact completion, and is equivalent to because the free functor from to is an equivalence of categories.
This construction could be generalized to any finitely complete category , from which the category of internal pseudo-equivalence relations of is the ex/lex completion of , and denoted as . If every epimorphism in is additionally a split epimorphism, then is its own free exact completion.
Many set-level type theories use types which are 0-truncated and thus h-sets by default because of the inclusion of uniqueness of identity proofs or axiom K to the rule system of the type theory. Sometimes, these type theories do not have quotients and image factorizations, and as a result, setoids are used instead of the native h-sets.
In homotopy type theory, and more generally in any intensional type theory where not all types are h-sets, such as in a type theory without uniqueness of identity proofs or axiom K, the notion of “setoid” bifurcates into multiple distinct notions. In analogy with category, the definitions used above in this article could be called a strict setoid. When the vertex types are only required to be a type rather than a set, then this defines a presetoid. There is also the notion of a univalent setoid, where equality of vertices is isomorphism of vertices in the core of a presetoid.
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
For setoids defined as a set with an pseudo-equivalence relation:
Olov Wilander, Constructing a small category of setoids, Mathematical Structures in Computer Science 22 1 (2012) 103-121 [doi:10.1017/S0960129511000478, pdf]
Erik Palmgren, Olov Wilander, Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science, 10 3 (2014) lmcs:964 [arXiv:1408.1364, doi:10.2168/LMCS-10(3:25)2014]
Jacopo Emmenegger, Erik Palmgren, Exact completion and constructive theories of sets, J. Symb. Log. 85 2 (2020) [arXiv:1710.10685, doi:10.1017/jsl.2020.2]
Cioffo Cipriano Junior, Def. 1.1.1 in: Homotopy setoids and generalized quotient completion [pdf, pdf]
Last revised on July 7, 2023 at 18:15:07. See the history of this page for a list of all contributions to it.